(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The following defined symbols can occur below the 0th argument of top: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of active: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of f: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of start: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of match: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of check: active, start, proper, top, f, check, match
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
match(f(x), f(y)) → f(match(x, y))
proper(f(x)) → f(proper(x))
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
proper(c) → ok(c)
f(mark(x)) → mark(f(x))
f(ok(x)) → ok(f(x))
active(f(x)) → f(active(x))
top(mark(x)) → top(check(x))
top(active(c)) → top(mark(c))
top(found(x)) → top(active(x))
check(f(x)) → f(check(x))
f(found(x)) → found(f(x))
active(f(x)) → mark(x)
start(ok(x)) → found(x)
match(X, x) → proper(x)
check(x) → start(match(f(X), x))
Rewrite Strategy: INNERMOST
(3) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6, 7]
transitions:
c0() → 0
ok0(0) → 0
mark0(0) → 0
found0(0) → 0
X0() → 0
proper0(0) → 1
f0(0) → 2
active0(0) → 3
top0(0) → 4
check0(0) → 5
start0(0) → 6
match0(0, 0) → 7
c1() → 8
ok1(8) → 1
f1(0) → 9
mark1(9) → 2
f1(0) → 10
ok1(10) → 2
check1(0) → 11
top1(11) → 4
active1(0) → 12
top1(12) → 4
f1(0) → 13
found1(13) → 2
found1(0) → 6
proper1(0) → 7
X1() → 16
f1(16) → 15
match1(15, 0) → 14
start1(14) → 5
ok1(8) → 7
mark1(9) → 9
mark1(9) → 10
mark1(9) → 13
ok1(10) → 9
ok1(10) → 10
ok1(10) → 13
c1() → 18
mark1(18) → 17
top1(17) → 4
found1(13) → 9
found1(13) → 10
found1(13) → 13
X2() → 21
f2(21) → 20
match2(20, 0) → 19
start2(19) → 11
check2(18) → 22
top2(22) → 4
X3() → 25
f3(25) → 24
match3(24, 18) → 23
start3(23) → 22
(4) BOUNDS(1, n^1)